implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
↳ QTRS
↳ DependencyPairsProof
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
IMPLIES(x, or(y, z)) → IMPLIES(x, z)
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
IMPLIES(x, or(y, z)) → IMPLIES(x, z)
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IMPLIES(x, or(y, z)) → IMPLIES(x, z)
Used ordering: Polynomial interpretation [25,35]:
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
The value of delta used in the strict ordering is 8.
POL(IMPLIES(x1, x2)) = (2)x_2
POL(not(x1)) = 0
POL(or(x1, x2)) = 4 + x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
The value of delta used in the strict ordering is 8.
POL(IMPLIES(x1, x2)) = (2)x_1 + (4)x_2
POL(not(x1)) = 4 + (2)x_1
POL(or(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))